<html>
<head><meta charset="utf-8"><title>correctness proofs · wg-secure-code · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/index.html">wg-secure-code</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html">correctness proofs</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="136125154"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136125154" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zach Reizner <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136125154">(Oct 19 2018 at 17:08)</a>:</h4>
<p>Stupid question: how do correctness proofs handle potentially buggy syscalls which break your assumptions?</p>



<a name="136125377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136125377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136125377">(Oct 19 2018 at 17:11)</a>:</h4>
<p>No. You have to either assume external stuff behaves in a certain way, or go and actually verify that external stuff.<br>
Which is why proven-correct mutex or semaphore implementation in Rust stdlib actually deadlocks when called recursively: Microsoft's implementation of the relevant OS primitive does not support it.</p>



<a name="136125868"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136125868" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zach Reizner <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136125868">(Oct 19 2018 at 17:18)</a>:</h4>
<p>I was going to ask more questions, but I don't know the first thing about software verification. <span class="emoji emoji-1f636" title="speechless">:speechless:</span> I'm going to go educate myself.</p>



<a name="136126012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136126012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136126012">(Oct 19 2018 at 17:20)</a>:</h4>
<p><span class="user-mention" data-user-id="132723">@Zach Reizner</span> solution: use seL4, prove your program correct in Isabelle, and build on their existing Isabelle proofs for seL4 <span class="emoji emoji-1f61c" title="stuck out tongue wink">:stuck_out_tongue_wink:</span></p>



<a name="136126040"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136126040" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zach Reizner <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136126040">(Oct 19 2018 at 17:20)</a>:</h4>
<p>If that was a joke, it went right over my head <span class="emoji emoji-1f60e" title="sunglasses">:sunglasses:</span></p>



<a name="136126054"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136126054" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136126054">(Oct 19 2018 at 17:21)</a>:</h4>
<p>It's a joke. They did 100,000 LoC of proofs for a 1,000 LoC program in C.</p>



<a name="136126059"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136126059" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136126059">(Oct 19 2018 at 17:21)</a>:</h4>
<p>it's also the recommended way you develop applications for seL4, heh</p>



<a name="136126069"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136126069" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136126069">(Oct 19 2018 at 17:21)</a>:</h4>
<p>...only to get what safe Rust already guarantees, assuming the stdlib and compiler are bug-free</p>



<a name="136126117"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136126117" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136126117">(Oct 19 2018 at 17:22)</a>:</h4>
<p>yup, yeah I'm personally in the "write the best Rust I can and hope that's good enough" department for now</p>



<a name="136126248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/correctness%20proofs/near/136126248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/correctness.20proofs.html#136126248">(Oct 19 2018 at 17:24)</a>:</h4>
<p>I'm really curious about applying SMACK to Rust now that it's been ported but didn't get a chance to really dig into it yet. I guess I'll repost this link in this topic too: <a href="http://soarlab.org/publications/atva2018-bhr.pdf" target="_blank" title="http://soarlab.org/publications/atva2018-bhr.pdf">http://soarlab.org/publications/atva2018-bhr.pdf</a> - this is an article from the guys who adapted it for Rust and got several programs verified. Seems like it would have caught the latest stdlib CVE too.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>